(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (not (and v6 v3 v5 v7 v17 q3 v1 q3 q1 q1))))
(assert v17)
(declare-const _17-0 (_ BitVec 17))
(assert v8)
(assert v11)
(assert (or (bvsle (bvurem (bvshl _17-0 _17-0) (bvshl _17-0 _17-0)) _17-0) v4 v13 v11 v2 v3 v12 v8 v3))
(declare-const v18 Bool)
(assert (= (bvsle (bvurem (bvshl _17-0 _17-0) (bvshl _17-0 _17-0)) _17-0) v13 v14 v7 v18 v7 v2 v3 v8 v9 v3))
(assert (= v10 v17 (bvule _17-0 _17-0)))
(check-sat)
